package com.um2.qualite;

public class Hanoi {

	private Tower[] towers=new Tower[3];;
	private int diskNB;
	
	//@ private model int towers_diskNB;
	//@ private represents towers_diskNB <- this.diskNB;

	//@ private model Tower tower0;
	//@ private represents tower0 <- towers[0];
	
	//@ private model Tower tower1;
	//@ private represents tower1 <- towers[1];
	
	//@ private model Tower tower2;
	//@ private represents tower2 <- towers[2];
	
	  //@ invariant this.towers_diskNB > 0 && this.towers_diskNB <= 10;
	
	/**Constructor of the gameboard : 3 towers  
	 * One tower contains 10 disk at maximum 
	 * @param diskNB The number of disk of the game it must be in [0..10]
	 **/
  	//@ ensures diskNB > 0 && diskNB <= 10;
	//@ requires tower0.getDiskNb()==diskNB;
	//@ requires tower1.isEmpty();
	//@ requires tower2.isEmpty();
	public Hanoi(int diskNB) {
		this.diskNB=diskNB;
		for (int i = 0; i < 3; i++) {
			towers[i] = new Tower(diskNB);
		}
		this.fillsTower(diskNB);
//		System.out.println(this.toString());
	}

	/**
	 * fill the first tower with i disks
	 * @param the nubmer of the diks in the first tower, in must be in [0..10]
	 */
	//@ requires tower0.getCapacity() >= i; 
	//@ ensures tower0.getDiskNb()==i;
	private void fillsTower(int i) {
		Disk d;
		int j=0;
		Tower t=towers[0];
		if(t.isEmpty()){
			j=i;
		}else{
				j=t.getTopDisk().getSize()-1;
		}
		while(t.getDiskNb()<i) {
			d = new Disk(j);
			j--;
			towers[0].push(d);
		}

	}

	/**
	 * @param i the index of the tower it must be in [0..2]
	 * @return The tower at i index
	 */
	//@ ensures i==0 ==> tower0 == \result; 
	//@ ensures i==1 ==> tower1 == \result;
	//@ ensures i==2 ==> tower2 == \result;
	private /*@ pure @*/ Tower getTower(int i) {
		return towers[i];

	}

	/**
	 * Move the top disk of the tower d1 to the top of the tower d2
	 * d1 musn't be empty !
	 * d2 musn't be full !
	 * @param d1 the tower with it top disk to move
	 * @param d2 the tower in witch we need to move the disk d1
	 */
	//@ requires getTower(d2).isStackable(getTower(d1).getTopDisk()); 
	//@ requires !(getTower(d1).isEmpty()); 
	//@ ensures getTower(d1).getDiskNb() == \old(getTower(d1).getDiskNb()-1) ;
	//@ ensures getTower(d2).getDiskNb() == \old(getTower(d2).getDiskNb()+1) ;
	public void moveDisk(int d1, int d2) {
		Disk d = this.getTower(d1).pop();
		this.getTower(d2).push(d);
	}

	/**
	 * The recursive function to solve the problem
	 * @param nbDisk
	 * @param d1
	 * @param d2
	 * @param inter
	 */
	public void moveDisks(int nbDisk, int departure,int arrival,int intermediate ){
	    if(nbDisk > 0){
	    	this.moveDisks(nbDisk-1, departure, intermediate,arrival);
	    	this.moveDisk(departure, arrival);
//	    	System.out.println(this.toString());
	    	this.moveDisks(nbDisk-1, intermediate,arrival,departure);
	    }
	}

	/**
	 * solve automatically the problem, with the recursive function
	 */
	//@ requires tower0.getDiskNb()==diskNB;
	//@ requires tower1.isEmpty();
	//@ requires tower2.isEmpty();
	//@ ensures tower0.isEmpty();
	//@ ensures tower1.isEmpty();
	//@ ensures tower2.getDiskNb()==diskNB;
	public void play() {
		moveDisks(this.diskNB, 0, 2, 1); 
	}

	/**
	 * Return a string representing the game configuration
	 */
	public String toString() {
		String res = "";
		for (int i = 0; i < 3; i++) {
			res = getTower(i).toString() + "\n^Tower " + (i) + "\n" + res;
		}
		return res + "--------HANOI BOARD-----------";

	}

}
